F, G:(), p:FinProbSpace, n:, X, Y:RandomVariable(p;n).
rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;(X.F(X)) o X;(Y.G(Y)) o Y) 

latex

Definitions	FinProbSpace, rv-disjoint(p;n;X;Y), left + right, P  Q, {T}, suptype(S; T), RandomVariable(p;n), #$n, Type, , s = t, (x.F(x)) o X, x. t(x), x(s), f(a), , {i..j}, , {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, S  T, x:AB(x), Outcome, x:A. B(x), t  T
Lemmas	p-outcome wf, rationals wf, rv-compose wf, not wf, int seg wf, finite-prob-space wf, nat wf, random-variable wf, rv-disjoint wf